w{-}rcvs($w$; $l$; $t$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$filter($\lambda$$a$.w{-}isrcvl($w$; $l$; $a$);map($\lambda$$t_{1}$.w{-}a($w$; destination($l$); $t_{1}$);upto($t$)))